Nuprl Definition : sendMinimalR
11,40
postcript
pdf
sendMinimalR{$a:ut2, $tg:ut2}
sendMinimalR
(
T
;
t
;
l
;
ds1
;
ds2
;
P
;
Q
;
d1
;
d2
;
f
)
==
([weakSendDoApplyR{$a:ut2, $tg:ut2}
==
([weakSendDoApplyR
(
T
;
t
;
l
;
ds1
;
f
o' mu'(
s
,
n
.
(
P
(
s
,
n
))));
==
([
weakSendDoApplyR{$a:ut2, $tg:ut2}
==
([weakSendDoApplyR
(
; 0; lnk-inv(
l
);
ds2
; mu'(
s
,
n
.
(
Q
(
s
,
n
))))])
latex
clarification:
sendMinimalR{$a:ut2, $tg:ut2}
sendMinimalR
(
T
;
t
;
l
;
ds1
;
ds2
;
P
;
Q
;
d1
;
d2
;
f
)
==
([weakSendDoApplyR{$a:ut2, $tg:ut2}
==
([weakSendDoApplyR
(
T
;
t
;
l
;
ds1
;
f
o' mu'(State(
ds1
);
s
,
n
.
(
P
(
s
,
n
));
d1
)) /
==
([
[weakSendDoApplyR{$a:ut2, $tg:ut2}
==
([[weakSendDoApplyR
(
; 0; lnk-inv(
l
);
ds2
; mu'(State(
ds2
);
s
,
n
.
(
Q
(
s
,
n
));
d2
)) /
==
([[
[]]])
latex
Definitions
(
L
)
,
f
o'
g
,
[
car
/
cdr
]
,
weakSendDoApplyR{$a:ut2, $tg:ut2}(
T
;
t
;
l
;
ds
;
f
)
,
,
#$n
,
lnk-inv(
l
)
,
mu'(
P
)
,
State(
ds
)
,
x
.
A
(
x
)
,
b
,
f
(
a
)
,
[]
origin